<!DOCTYPE HTML>
<html><head><meta charset="utf-8"><title>Inline</title><link rel="stylesheet" href="Agda.css"></head><body><pre><a id="1" class="Background">\documentclass{article}

\usepackage{agda}

\begin{document}

Assume that we are given a type
%
</a><a id="97" class="Markup">\begin{code}[hide]</a>
  <a id="118" class="Keyword">module</a> <a id="125" href="Inline.html" class="Module">_</a> <a id="127" class="Symbol">(</a>
<a id="129" class="Markup">\end{code}</a><a id="139" class="Background">
</a><a id="140" class="Markup">\begin{code}[inline]</a>
    <a id="165" href="Inline.html#165" class="Bound">A</a> <a id="167" class="Symbol">:</a> <a id="169" class="PrimitiveType">Set</a>
<a id="173" class="Markup">\end{code}</a><a id="183" class="Background">
</a><a id="184" class="Markup">\begin{code}[hide]</a>
    <a id="207" class="Symbol">)</a> <a id="209" class="Symbol">(</a>
<a id="211" class="Markup">\end{code}</a><a id="221" class="Background">
%
,
and that a function
%
</a><a id="248" class="Markup">\begin{code}[inline*]</a>
    <a id="274" href="Inline.html#274" class="Bound">F</a> <a id="276" class="Symbol">:</a> <a id="278" class="PrimitiveType">Set</a> <a id="282" class="Symbol">→</a> <a id="284" class="PrimitiveType">Set</a> <a id="288" class="Symbol">→</a> <a id="290" class="PrimitiveType">Set</a> <a id="294" class="Symbol">→</a> <a id="296" class="PrimitiveType">Set</a>
<a id="300" class="Markup">\end{code}</a><a id="310" class="Background">
</a><a id="311" class="Markup">\begin{code}[hide]</a>
    <a id="334" class="Symbol">)</a> <a id="336" class="Keyword">where</a>
<a id="342" class="Markup">\end{code}</a><a id="352" class="Background">
%
is also given.

\end{document}
</a></pre></body></html>